Termination w.r.t. Q proof of TRS/AProVEAAECC-ring.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.

↳ QTRS

  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.

We have applied [15,7] to switch to innermost. The TRS R 1 is

sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)

The TRS R 2 is

ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The signature Sigma is {if_5, if_2, ring, if_3, if_4, if_1, if_7, if_8, if_6, if_9}

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
APP(cons(h, t), x) → APP(t, x)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
LENGTH(cons(h, t)) → LENGTH(t)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
APP(cons(h, t), x) → APP(t, x)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
LENGTH(cons(h, t)) → LENGTH(t)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
APP(cons(h, t), x) → APP(t, x)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
LENGTH(cons(h, t)) → LENGTH(t)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
LEQ(s(n), s(m)) → LEQ(n, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 45 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(cons(h, t), x) → APP(t, x)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APP(cons(h, t), x) → APP(t, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2) = APP(x1)
cons(x1, x2) = cons(x1, x2)

Recursive Path Order [2].
Precedence:

cons₂ > APP₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
MAP_F(x1, x2) = MAP_F(x2)
cons(x1, x2) = cons(x1, x2)

Recursive Path Order [2].
Precedence:

cons₂ > MAP_F₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(h, t)) → LENGTH(t)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LENGTH(cons(h, t)) → LENGTH(t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LENGTH(x1) = LENGTH(x1)
cons(x1, x2) = cons(x1, x2)

Recursive Path Order [2].
Precedence:

cons₂ > LENGTH₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(s(n), s(m)) → LEQ(n, m)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LEQ(s(n), s(m)) → LEQ(n, m)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LEQ(x1, x2) = LEQ(x2)
s(x1) = s(x1)

Recursive Path Order [2].
Precedence:

s₁ > LEQ₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SNDSPLIT(x1, x2) = SNDSPLIT(x2)
s(x1) = s
cons(x1, x2) = cons(x1, x2)

Recursive Path Order [2].
Precedence:

s > SNDSPLIT₁
cons₂ > SNDSPLIT₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
FSTSPLIT(x1, x2) = FSTSPLIT(x2)
s(x1) = s
cons(x1, x2) = cons(x1, x2)

Recursive Path Order [2].
Precedence:

s > FSTSPLIT₁
cons₂ > FSTSPLIT₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))

The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

The set Q consists of the following terms:

fstsplit(0, x0)
fstsplit(s(x0), nil)
fstsplit(s(x0), cons(x1, x2))
sndsplit(0, x0)
sndsplit(s(x0), nil)
sndsplit(s(x0), cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
length(nil)
length(cons(x0, x1))
app(nil, x0)
app(cons(x0, x1), x2)
map_f(x0, nil)
map_f(x0, cons(x1, x2))
head(cons(x0, x1))
tail(cons(x0, x1))
ring(x0, x1, x2, x3, x4, x5)
if_1(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, true)
if_3(x0, x1, x2, x3, x4, x5, false)
if_2(x0, x1, x2, x3, x4, x5, false)
if_4(x0, x1, x2, x3, x4, x5, false)
if_5(x0, x1, x2, x3, x4, x5, true)
if_6(x0, x1, x2, x3, x4, x5, true)
if_7(x0, x1, x2, x3, x4, x5, false)
if_6(x0, x1, x2, x3, x4, x5, false)
if_8(x0, x1, x2, x3, x4, x5, false)
if_9(x0, x1, x2, x3, x4, x5, true)

We have to consider all minimal (P,Q,R)-chains.